the_w:World, e:E.
FairFifo
 (isrcv(kind(e)))
 (t:{0..time(e)}
 (((match(lnk(kind(e));t;time(e)))
 (& (((0  (||rcvs(lnk(kind(e));time(e))|| - ||snds(lnk(kind(e));t)||))
 (& (& ((||rcvs(lnk(kind(e));time(e))|| 
 (& (& (- ||snds(lnk(kind(e));t)||) < ||onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))||))
 (& (c (onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))|| 
 (& (c (- ||snds(lnk(kind(e));t)||)]
 (& (c (=
 (& (c (msg(a(loc(e);time(e)))
 (& (c ( Msg)))) 

latex

Definitions

x:A. B(x), P  Q, t  T, isrcv(l;a), kind(e), loc(e), time(e), t.1, t.2, act(e), b, p  q, b, , T, True, tt, if b then t else f fi , ff, queue(l;t), Top, S  T, P & Q, P  Q, P  Q, , match(l;t;t'), SQType(T), {T}, A, A  B, False, {i..j}, i  j < k, FairFifo, A c B, E, SqStable(P), , Unit, i  j , hd(l), snds(l;t), x:A. B(x),

Lemmas

assert wf, isrcv wf, w-ekind wf, fair-fifo wf, w-E wf, world wf, sq stable from decidable, band wf, bnot wf, w-isnull wf, w-a wf, w-kind wf, eq lnk wf, lnk wf, decidable assert, bool wf, eqtt to assert, iff transitivity, not wf, eqff to assert, assert of bnot, assert-eq-lnk, w-loc wf, w-time wf, length wf nat, w-rcvs wf, top wf, w-action wf, nat wf, w-snds wf, w-Msg wf, ge wf, squash wf, true wf, general length nth tl, length wf1, lt int wf, assert of lt int, le int wf, le wf, bnot of lt int, assert of le int, nth tl decomp, w-msg wf, IdLnk wf, select wf, select concat, map wf, int seg wf, w-ml wf, upto wf, concat wf, map length, length upto, firstn map, firstn upto, bnot of le int